Crate polytype[−][src]

A Hindley-Milner polymorphic typing system.

For brevity, the documentation heavily uses the two provided macros when creating types.

A TypeSchema is a type that may have universally quantified type variables. A Context keeps track of assignments made to type variables so that you may manipulate Types, which are unquantified and concrete. Hence a TypeSchema can be instantiated, using TypeSchema::instantiate, into a Context in order to produce a corresponding Type. Two Types under a particular Context can be unified using Context::unify, which may record new type variable assignments in the Context.

Examples

The basics:

use polytype::Context;

// filter: ∀α. (α → bool) → [α] → [α]
let t = ptp!(0; @arrow[
    tp!(@arrow[tp!(0), tp!(bool)]),
    tp!(list(tp!(0))),
    tp!(list(tp!(0))),
]);

// Quantified type schemas provide polymorphic behavior.
assert_eq!(t.to_string(), "∀t0. (t0 → bool) → list(t0) → list(t0)");

// We can instantiate type schemas to remove quantifiers
let mut ctx = Context::default();
let t = t.instantiate(&mut ctx);
assert_eq!(t.to_string(), "(t0 → bool) → list(t0) → list(t0)");

// We can register a substiution for t0 in the context:
ctx.extend(0, tp!(int));
let t = t.apply(&ctx);
assert_eq!(t.to_string(), "(int → bool) → list(int) → list(int)");

Extended example:

use polytype::Context;

// reduce: ∀α. ∀β. (β → α → β) → β → [α] → β
// We can represent the type schema of reduce using the included macros:
let t = ptp!(0, 1; @arrow[
    tp!(@arrow[tp!(1), tp!(0), tp!(1)]),
    tp!(1),
    tp!(list(tp!(0))),
    tp!(1),
]);
assert_eq!(t.to_string(), "∀t0. ∀t1. (t1 → t0 → t1) → t1 → list(t0) → t1");

// Let's consider reduce when applied to a function that adds two ints

// First, we create a new typing context to manage typing bookkeeping.
let mut ctx = Context::default();

// Let's create a type representing binary addition.
let tplus = tp!(@arrow[tp!(int), tp!(int), tp!(int)]);
assert_eq!(tplus.to_string(), "int → int → int");

// We instantiate the type schema of reduce within our context
// so new type variables will be distinct
let t = t.instantiate(&mut ctx);
assert_eq!(t.to_string(), "(t1 → t0 → t1) → t1 → list(t0) → t1");

// By unifying, we can ensure function applications obey type requirements.
let treturn = ctx.new_variable();
let targ1 = ctx.new_variable();
let targ2 = ctx.new_variable();
ctx.unify(
    &t,
    &tp!(@arrow[
        tplus.clone(),
        targ1.clone(),
        targ2.clone(),
        treturn.clone(),
    ]),
).expect("unifies");

// We can also now infer what arguments are needed and what gets returned
assert_eq!(targ1.apply(&ctx), tp!(int));             // inferred arg 1: int
assert_eq!(targ2.apply(&ctx), tp!(list(tp!(int))));  // inferred arg 2: list(int)
assert_eq!(treturn.apply(&ctx), tp!(int));           // inferred return: int

// Finally, we can see what form reduce takes by applying the new substitution
let t = t.apply(&ctx);
assert_eq!(t.to_string(), "(int → int → int) → int → list(int) → int");

Macros

ptp	Creates a `TypeSchema` (convenience for common patterns).
tp	Creates a `Type` (convenience for common patterns).

Structs

Context	A type environment. Useful for reasoning about `Type`s (e.g unification, type inference).
ContextChange	Allow types to be reified for use in a different context. See `Context::merge`.

Enums

Type	Represents monotypes (fully instantiated, unquantified types).
TypeSchema	Represents polytypes (uninstantiated, universally quantified types).
UnificationError	Errors during unification.

Traits

Name	Types require a `Name` for comparison.

Type Definitions

Variable

Represents a type variable (an unknown type).